COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%frame[w87,jmc]		The frame problem today
C00004 00003	\section{Introduction}
C00006 00004	\section{Frame axioms}
C00008 00005	\section{Frames}
C00013 00006	\centerline{This draft of \jobname\ TEXed on \jmcdate\ at \theTime}
C00014 00007	notes: see frame[f86,jmc]
C00025 00008	This probably doesn't go in this paper.
C00027 00009	\noindent Remark: A damnfool complexity theorem
C00029 ENDMK
C⊗;
%frame[w87,jmc]		The frame problem today
\input memo.tex[let,jmc]
\title{The Frame Problem Today}

\noindent Abstract: AI systems that do prediction or planning need to
represent information about the effects of actions and other events.  When
an event occurs, some things change and others don't, and this has to be
described.  The frame problem concerns how to describe efficiently what
doesn't change.  If there are $n$ kinds of events and $m$ properties, we
want to avoid putting $O(mn)$ facts in the database most of which would
express information like ``When an object is moved, other objects don't
change their colors except if $\ldots$''.  The frame problem is most severe
when large databases of general common sense knowledge are proposed.
This paper discusses various mechanisms for dealing with the frame
problem, concentrating on logical formalisms and concentrating further on
those involving non-monotonic reasoning.
\vfill\eject
\section{Introduction}

	AI systems that do prediction or planning need to represent
information about the effects of actions and other events.  When an event
occurs, some things change and others don't, and this has to be described.
The frame problem concerns how to describe efficiently what doesn't
change.  If there are $n$ kinds of events and $m$ properties, we want to
avoid putting $O(mn)$ facts in the database most of which would express
information like ``When an object is moved, other objects don't change
their colors except if $\ldots$''.  The frame problem is most severe when
large databases of general common sense knowledge are proposed.  This
paper discusses various mechanisms for dealing with the frame problem,
concentrating on logical formalisms and concentrating further on those
involving non-monotonic reasoning.

	The frame problem was first mentioned in (McCarthy and Hayes 1970)
and not sufficiently clearly explained.  It has been more recently called
the persistence problem, and maybe that's a better name.
\section{Frame axioms}

	Suppose we use a situation calculus (McCarthy and Hayes 1970)
formalism.  The following axioms describe the effects of moving and
painting blocks.

$$\displaylines{∀x l s.clear(top(x),s) ∧ clear(l,s) ∧ ¬tooheavy(x)\hfill\cr
\hfill ⊃ loc(x,result(move(x,l),s)) = l\cr}$$
$$\displaylines{∀x c s.color(x,result(paint(x,c),s)) = c.\hfill\cr}$$
\medskip
\itemb Frame axioms:
$$∀x y l s.color(y,result(move(x,l),s)) = color(y,s).$$
$$∀x y l s.y ≠ x ⊃ loc(y,result(move(x,l),s)) = loc(y,s).$$
$$∀x y c s.loc(x,result(paint(y,c),s)) = loc(x,s).$$
$$∀x y c s.y ≠ x ⊃ color(x,result(paint(y,c),s)) = color(x,s).$$
\medskip

All qualifications are given in the axioms, and a full statement
is given of what doesn't change when an action occurs.
\section{Frames}

	Frames are a device for dealing with the frame problem.
The name comes from the use of co-ordinate frames in geometry or
from state vectors in computer science.
(McCarthy 1963) %Towards ...
presents an axiomatization of assignment statements.  In these
axioms, $\xi$ represents a state, $var$ represents a variable and
$val$ represents a value of a variable.  We use two functions
$c(var,\xi)$ giving the {\it contents} of $var$ in the
state $\xi$ and $a(var,val,\xi)$ giving the new state $\xi '$
that results when $var$ is given the new value $val$ in the
state $\xi$.  Here are the axioms for assignment.
%
$$∀var val \xi.c(var,a(var,val,\xi)) = val,$$
%
$$∀var1 var val \xi.var1 ≠ var ⊃ c(var1,a(var,val,\xi)) = c(var1,\xi),$$
%
$$∀var val1 val2 \xi.a(var,val2,a(var,val1,\xi)) = a(var,val2,\xi),$$
%
$$∀var1 var2 val1 val2 \xi.var1 ≠ var2 ⊃ a(var1,val1,a(var2,val2,\xi)) =
a(var2,val2,a(var1,val1,\xi))$$
%
and
%
$$∀\xi1 \xi2.(∀var.c(var,\xi1)=c(var,\xi2)) ⊃ \xi1 = \xi2.$$
%
	In these axioms the variable $\xi$ can be considered as associated
with a {\it co-ordinate frame}, and the axioms assert that when one
of the co-ordinates is assigned a new value {\it relative to the frame},
the other co-ordinates don't change their values.  The last axiom,
a kind of extensionality, is sometimes omitted.  The ``frame problem''
took its name from some such notion of frame.

	The simplest way of applying these axioms to the situation
calculus is to treat situations as frames, i.e. to use the situation
$s$ where the state variable $\xi$ was used.  This has disadvantages,
which we will discuss, but first let's put the axioms for moving and
painting into this form.

$$∀x l s.clear(top x, s) ∧ clear(l,s) ∧ ¬tooheavy x
⊃ result(move(x,l),s) = a(loc x,l,s)$$
%
and
%
$$∀x c s.result(paint(x,c),s) = a(color x,c,s).$$

\noindent No axioms about what doesn't change are required, because
that is taken care of by the general axioms for assignment.
Notice that fluents are reified and that ``primitive fluents''
play a role like that of variables in assignment statements.

	In order to prove that something doesn't
change, we have to use the inequalities in the assignment axioms,
and this requires proving that the fluents are distinct, i.e. we
must be able to prove statements like $∀x y.x ≠ y ⊃ loc x ≠ loc y$ and
$∀x y.loc x ≠ color y$.  At first sight it looks as if $O(n↑2)$
axioms would be required to assert this for $n$ fluents.  We leave
as an exercise for the reader showing how to do it with $O(n)$
axioms.

	Making the situation into a single grand state vector
may be too strong for some axiomatizations.  We can then imagine
that the situation variable has a number of frames attached to
it.  For example, suppose that the frame $F1$ contains both the
color and the position of the blocks in some set attached to it.
Then the axiom describing coloring blocks takes the form
%
$$∀x s c.val(F1,result(paint(x,c),s)) = a(color x,l,val(F1,s)).$$
%
Here $val(F1,s)$ is the ``local'' state vector of the frame $F1$.
\centerline{This draft of \jobname\ TEXed on \jmcdate\ at \theTime}
\centerline{Copyright \copyright\ \number\year\ by John McCarthy}
\vfill\eject\end
notes: see frame[f86,jmc]

	McDermott says that logic is inefficient but doesn't compare it
with anything specific.

	There is an impression (McDermott 1987) that persistence arguments
in logic are impractical.  This could mean either that they are difficult
to find or that they are necessarily long.  We are not prepared to discuss
the heuristic problem in this paper, but we can show that the arguments
are not necessarily long.  How long they are depends on what is reified.
Here is an informal description of how to keep them short.

	Suppose we have a sequence of events, and we need to determine
what has not changed after the the sequence has occurred.  It looks
like we need to reify both sequences of events and sets of fluents.
If each event of the sequence modifies only fluents of the set $A$,
then clearly the sequence itself only modifies these fluents.

Why aren't frames adequate?  There is no subjective evidence for them.
In itself this doesn't preclude their use in AI; maybe they are better
than what nature has evolved for humans.  However, it provides grounds
for doubt.  However, there is a more concrete objection.  One of the
major objectives of the logic approach to AI is to enable a system
to learn or be told facts independently.  If a new fluent must be
attached to a frame, then whoever tells the system must either know
about the frame or there must be a general mechanism whereby facts
as received are attached to appropriate frames.

McDermott says, ``$\ldots$ it (the frame problem) is mainly a problem
for the logicist approach''.  He also speaks of ``AI practitioners''
not knowing about it.  He is right in so far as AI practitioners in 1987
don't have the ambitions of (McCarthy 1960).  That paper proposed that
AI systems should share with humans the ability to learn facts
independently of one another.  In particular humans can be told
about new fluents and what changes them and can integrate this
new information with what they already know.  When one builds
a system with a fixed set of fluents, the problem can be avoided
in a variety of ways.

  Indeed the frame problem can be avoided
provided one is not very ambitious.  STRIPS solved it at the price
of allowing the expression of only facts true in a single situation,
not permitting comparison of different situations.  Using frames,
as described above, solves it within the logic approach.  The price
is that each fluent introduced must be classified as being primitive
or not, and if primitive, must be attached to a frame.  This doesn't
meet the goal of allowing facts to be learned independently as
proposed in (McCarthy 1960).  It is now 1987, and most ``AI
practitioners'' don't build systems that can learn about new
fluents.

``Most steps of a proof about time will be aimed at proving that
something is still true in a given situation by stringing together
such axioms.''

  Presumably McDermott means a proof about the results
of actions rather than a proof about time per se.  (I mention the
point, because it seems to me that much of the effort put into
pure theories of time is misguided, because what AI really needs
is improved theories of action).

I am grateful to McDermott for expressing all these misconceptions,
since it provides me motivation to be explicit about a large number of
points which I had supposed would readily be apparent from the general
formalism as soon as a need for efficiency developed.

Suppose a robot needs to prove a proposition $holds(p,S↓{1000})$, where
$S↓{1000}$ is the situation that results from a situation $S↓0$ after
1000 actions.  We suppose that it needs it as a precondition for
the successful performance of an action.  Suppose further that $p$
holds, because none of the 1000 actions affected it.  How many
proof steps are required to establish this?  Since we expect such
proofs to be required often, some machinery aimed at making it
easy is justified.  Therefore, we propose reifying sets of fluents,
so let $Foo$ be a set of primitive fluents such that it can be shown
that the sequence $(a↓1,\ldots,a↓{1000})$ of actions can affect only
these primitive fluents.  The proof of this may take 1000 steps if
each action is considered separately, but it may be possible to say
that all the actions are in a set that affects only the primitive
fluents of $Foo$.  For example, if all the actions involve moving
blocks, then it is a theorem that any sequence affects only locations
of blocks.  In that case it is a single step to show that the 1000
action sequence doesn't affect the colors of any blocks.

	I think readers, including McDermott, should readjust their
intuitions until the above argument becomes intuitively obvious.
namely, if it is apparent to a human that a long sequence of actions
each of which only moves blocks will affect only the locations of
the blocks, then in an axiomatization that corresponds reasonably
to the human knowledge of the matter, the fact will have a short
proof.  Of course, this may not turn out to be the most immediately
obvious axiomatization in the reader's understanding of how to
axiomatize.  The simplest axiomatizations don't reify enough to
allow short proofs about long sequences of actions.

	I want to refute the possible complaint that the axiomatization
would have to be ad hoc, i.e. based on a prior understanding of exactly
what is to be proved.  Therefore, I want to propose some general
principles.  First, if objects of type $X$ are reified, then sets
and sequences of objects of type $X$ should also be allowed in
the formalism.  This is essentially a proposal to include the
set forming operations and the set theory axioms of ZF, Zermelo-Frankel
set theory, in logical systems that are expected to have short proofs.
However, we may need more.  Namely, if the system is to be able to
reason about its future knowledge or that of other agents, it needs
to reify concepts.  (McCarthy 1979)%First order theories if individual ...
contains proposals for reifying concepts.  We propose that if the
system contains reifies a type of object, it also reify concepts of
objects of this type.

	This not only requires more than has been put in any AI program to
date.  It is even more than has been put in any system of axioms for AI.
It will be required when it is necessary for systems to handle large
numbers of facts, fluents and concepts and consider strategies that
may result in long sequences of actions.  (Did I forget, strategies
must be reified also).  As long as we are considering special issues,
e.g. the frame and qualification problems, we can make do with much
simpler systems of axioms.

****

When is there no frame problem?

Something must be said about the computability of circumscription.

This probably doesn't go in this paper.
	All I know about Y is A.  Here Y is a set of predicates and
A is a sentence.  It means that any interpretation of Y compatible
with A is possible, e.g. true in some possible world.  This can
be expressed in a logic of one higher order than the predicates in Y.
It may be that this needs generalization along the lines of the way
VAL's pointwise circumscription generalizes ordinary circumscription.
Namely, we may fix certain arguments of the predicates, and all
we know about the predicates for these arguments is A.  If we want
to talk about knowledge about knowledge, that's ok if the hierarchy
is well-founded in some appropriate sense.
\noindent Remark: A damnfool complexity theorem

	The above considerations almost surely will lead someone to
prove what I call a damnfool complexity theorem, e.g. though probably
there won't be a variant of this prediction problem that is NP-complete.
Namely, suppose we have $m$ different actions and $n$ primitive
fluents, and which actions affect which fluents is completely
random, i.e. there are no natural classes of actions and fluents,
and whether an action affects a fluent depends on the values of
all the fluents.  Then it can indeed turn out that proving that a
sequence of $k$ actions doesn't affect a certain fluent requires
tracing all the fluents through the complete sequence of actions.
Of course, this corresponds to a situation in which humans also
can't easily determine whether the fluent is affected.